the_es:ES. Trans x,y:E. x  y  

latex

Definitions	x:A. B(x), ES, t  T, E, Prop, (e <loc e'), P  Q, P  Q, Trans x,y:T. E(x;y), e  e' , {T}
Lemmas	es-locl wf, es-E wf, event system wf, es-locl-trans